Iof proof for Lemma comb for int upper wf:
(
n,z. {n...}) 
(
True)Type
by (ProveOpCombinatorTyping (Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
)) (first_tok :t) inil_term)) `int_upper_wf`
.| 9,38 |
(n,z. {n...}) (True)Type
by (ProveOpCombinatorTyping (Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
)) (first_tok :t) inil_term)) `int_upper_wf`
.
| Definitions | T  x:A. B(x)T |
| Lemmas |